\section{Post-Pre Condition}

\begin{theorem}[Input Given Output with String]
Given an SST $\sst$ from $\sstinputalph$ to $\sstoutputalph$ and a string $a$, the language $A$ such that $\brac{T}(A)=a$
(and $\brac{T}(\sstinputalph\st\setminus A)\not = a$) is effectively computable in time
$\bigo{((|\sstinputalph|+|\sstvars|)^{|a|+|\sstvars|}})$ and is regular.
\end{theorem}
\Proof
We build a NFA $N_a=(Q_N,\sstinputalph,\delta_N,Q_N^i,F_N)$ such that $L(N)=A$.
Every state in $Q_N$ is going to be a pair $(q,e)$ where $q\in \sststates$ is a state of $\stt$ and $e\in (\sstoutputalph\cup \sstvars)\st$
is a summarization of the value of the output function.

To build the $N_a$ we use a fix point algorithm that iteratively add states. We start with the set of states
$Q_N=F_N=\{(q,e)| F(q)\ is\ defined \wedge F(q)=e\}$, $\delta_N$ always $\emptyset$ and $Q_N^i=\emptyset$.
Then we compute $Q'_N$ doing back propagation and we stop the algorithm when $Q'_N=Q_N$. We then set $Q_N^i$ to
$\{(q,e)|(q,e)\in Q_N \wedge [\emptystring/\sstvars]e=a\}$ (where $[\emptystring/\sstvars]e$ is $e$ in which
we substitute every variable with $\emptystring$.

The back propagation algorithm is the following: set $Q'_N=Q_N$ then,
$\forall (q,e)\in Q_N. \forall q'\in\sststates. \forall a\in\sstinputalph.
if\ \sststtr(q',a)=q \wedge [\sstvarup(q,a,\sstvars)/\sstvars]e=e' \wedge |e'|\leq |a|+|\sstvars|\ then\
Q'_N=Q'_N\cup \{(q',e')\} \wedge \delta_n((q,e),a)=\delta_n((q,e),a)\cup \{(q',e')\}$.

With the restriction $|e'|\leq |a|+|\sstvars|$ we bound the size of the equation. Since the assignment are copyless
every variable can appear at most once in $e'$ and if $|e'|> |a|+|\sstvars|$ the equation $e=a$ can't admit any solution.

Let's sketch the proof of correctness. We want every string in $s\in A$ to be generated by $N$ and viceversa.
If $s=s_1\ldots s_n$ we'll have that there exists a run $(q_0,\alpha_0),\ldots,(q_n,\alpha_n)$ in $\sst$
such that $[\alpha_n/\sstvars]F(q_n)=a$ and $\sttsttr(q_i,s_{i+1})=q_{i+1}$. By definition $F_N$
will contain the state $(q_n,F(q_n))$ (let's call $F(q_n)$ $e_n$).
Now we basically maintain the invariant that for every $(q_i,e_i)$, $[\alpha_i/\sstvars]e_i=a$. Since this is
immediate by construction we are done (for the $\Leftarrow$ direction). For the other direction the idea is similar. If
such a path exists there must be an initial \emph{all-epsilon} equation that leads to the final answer containing only the
variables that will contribute to the output.
\qed


\begin{theorem}[Succinctness]
For every $k\in \mathbb{N}$ there exist an SST $\sst_k:\sstinputalph_k\rightarrow\sstoutputalph_k$ and a string $a_k\in\sstoutputalph_k\st$
such that the minimal NFA $I$ such that $\brac{T_k}(I)=a$ has size $\bigo((|\sstinputalph|+|\sstvars|)^{|I|+|\sstvars|})$
and the corresponding minimal DFA has size $\bigo(\ldots)$

\end{theorem}
\Proof
Don't have one
\qed

\begin{theorem}[Input Given Output with Regular Expression]
Given an SST $\sst$ from $\sstinputalph$ to $\sstoutputalph$ and a DFA $O$, the language $I$ such that $\brac{T}(I)\in L(O)$
(and $\brac{T}(\sstinputalph\st\setminus I)\cap L(O)=\emptyset$) is regular and effectively computable in time $\bigo(2^{...})$.
\end{theorem}
\Proof
Don't have one
\qed 